Search for: All records

Abstract This paper addresses the compensation of wave actuator dynamics in scalar extremum seeking (ES) for static maps. Infinite-dimensional systems described by partial differential equations (PDEs) of wave type have not been considered so far in the literature of ES. A distributed-parameter-based control law using back-stepping approach and Neumann actuation is initially proposed. Local exponential stability as well as practical convergence to an arbitrarily small neighborhood of the unknown extremum point is guaranteed by employing Lyapunov–Krasovskii functionals and averaging theory in infinite dimensions. Thereafter, the extension for wave equations with Dirichlet actuation, antistable wave PDEs as well as the design for the delay-wave PDE cascade are also discussed. Numerical simulations illustrate the theoretical results. 

We present a high-assurance and high-speed implementation of the SHA-3 hash function. Our implementation is written in the Jasmin programming language, and is formally verified for functional correctness, provable security and timing attack resistance in the EasyCrypt proof assistant. Our implementation is the first to achieve simultaneously the four desirable properties (efficiency, correctness, provable security, and side-channel protection) for a non-trivial cryptographic primitive. Concretely, our mechanized proofs show that: 1) the SHA-3 hash function is indifferentiable from a random oracle, and thus is resistant against collision, first and second preimage attacks; 2) the SHA-3 hash function is correctly implemented by a vectorized x86 implementation. Furthermore, the implementation is provably protected against timing attacks in an idealized model of timing leaks. The proofs include new EasyCrypt libraries of independent interest for programmable random oracles and modular indifferentiability proofs.